/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.checker;

import static com.googlecode.syper.javasyp.checker.Substitution.replace;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;
import java.util.logging.Logger;

import org.eclipse.jdt.core.dom.AST;
import org.eclipse.jdt.core.dom.ASTNode;
import org.eclipse.jdt.core.dom.ArrayAccess;
import org.eclipse.jdt.core.dom.ArrayCreation;
import org.eclipse.jdt.core.dom.ArrayInitializer;
import org.eclipse.jdt.core.dom.AssertStatement;
import org.eclipse.jdt.core.dom.Assignment;
import org.eclipse.jdt.core.dom.Block;
import org.eclipse.jdt.core.dom.BreakStatement;
import org.eclipse.jdt.core.dom.ClassInstanceCreation;
import org.eclipse.jdt.core.dom.ConditionalExpression;
import org.eclipse.jdt.core.dom.ConstructorInvocation;
import org.eclipse.jdt.core.dom.ContinueStatement;
import org.eclipse.jdt.core.dom.DoStatement;
import org.eclipse.jdt.core.dom.EnhancedForStatement;
import org.eclipse.jdt.core.dom.Expression;
import org.eclipse.jdt.core.dom.FieldAccess;
import org.eclipse.jdt.core.dom.ForStatement;
import org.eclipse.jdt.core.dom.IBinding;
import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.IfStatement;
import org.eclipse.jdt.core.dom.InfixExpression;
import org.eclipse.jdt.core.dom.LabeledStatement;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.MethodInvocation;
import org.eclipse.jdt.core.dom.Modifier;
import org.eclipse.jdt.core.dom.PostfixExpression;
import org.eclipse.jdt.core.dom.PrefixExpression;
import org.eclipse.jdt.core.dom.QualifiedName;
import org.eclipse.jdt.core.dom.ReturnStatement;
import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.SingleVariableDeclaration;
import org.eclipse.jdt.core.dom.Statement;
import org.eclipse.jdt.core.dom.SuperConstructorInvocation;
import org.eclipse.jdt.core.dom.SuperMethodInvocation;
import org.eclipse.jdt.core.dom.ThisExpression;
import org.eclipse.jdt.core.dom.TypeDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclaration;
import org.eclipse.jdt.core.dom.VariableDeclarationFragment;
import org.eclipse.jdt.core.dom.WhileStatement;
import org.eclipse.jdt.core.dom.InfixExpression.Operator;

import com.googlecode.syper.anno.Pred.IntPred;
import com.googlecode.syper.javasyp.checker.IChecker.Category;
import com.googlecode.syper.javasyp.config.JavaSypPreferences;
import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.FormulaVisitor;
import com.googlecode.syper.javasyp.formulae.Infix;
import com.googlecode.syper.javasyp.formulae.Literal;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Name;
import com.googlecode.syper.javasyp.formulae.Prefix;
import com.googlecode.syper.javasyp.formulae.Quantifier;
import com.googlecode.syper.javasyp.formulae.Ref;
import com.googlecode.syper.javasyp.formulae.Select;
import com.googlecode.syper.javasyp.formulae.Store;
import com.googlecode.syper.javasyp.prover.Prover;
import com.googlecode.syper.javasyp.prover.ProverResult;
import com.googlecode.syper.javasyp.prover.ProverResult.Status;

/**
 * @author kevin
 *
 */
abstract class AbstractLogicMethodVisitor<L extends AbstractHavocLookup<L>> extends SymbolicMethodVisitor {

	private static final Logger log = Logger.getLogger(AbstractLogicMethodVisitor.class.getName());

	private Set<Formula> knowledge;

	private L lookup;
	/** method parameter pre-image for {@code \old} in assertions and post-conditions */
	private L preLookup;

	private final Prover prover;

	private boolean nullChecks = false;
	private boolean boundsChecks = false;
	private boolean concurrentChecks = false;

	private final List<Boolean> nullCheckStack = new ArrayList<Boolean>();
	private final List<Boolean> boundsCheckStack = new ArrayList<Boolean>();

	/** Set to <code>true</code> to check if assumptions lead to contradiction */
	private boolean smoke = false;

	private boolean useArrayStore = false;

	/**
	 * stupid, stupid, stupid: so we know in {@link #endVisit(MethodDeclaration)}
	 * that we didn't visit a nested inner class.
	 */
	private boolean isNested;

	protected AbstractLogicMethodVisitor() {
		this.prover = createProver();
	}

	@Override
	public long getSolverMillis() {
		return prover.getSolverMillis();
	}

	public void setConcurrentChecks(boolean enable) {
		concurrentChecks = enable;
	}

	public void setSmoke(boolean smoke) {
		this.smoke = smoke;
	}

	@Override
	public boolean preVisit2(ASTNode node) {
		if (getChecker().isCanceled()) {
			log.info("Checker has been canceled by user");
			return false;
		}
		return super.preVisit2(node);
	}

	protected L getLookup() {
		return lookup;
	}

	@Override
	public boolean visit(MethodDeclaration node) {
		boolean result = super.visit(node);
		pushFlags(node.resolveBinding());

		isNested = knowledge != null;
		if (isNested) {
			// TODO anonymous inner classes....
			getChecker().reportUserProblem("Nested inner classes not supported: skipping", node, Category.UNSUPPORTED);
			return false;
		}
		knowledge = new LinkedHashSet<Formula>();
		lookup = createLookup(node.getAST());
		prover.setContext(node.resolveBinding().getKey());

		if (getReceiver() != null)
			assume(Prefix.not(Infix.equals(
					lookup.getReceiver(getReceiver()),
					Literal.NULL)));

		Contract c = getChecker().getContract(node);
		if (c != null && (c.getPre() != null || c.getPost() != null)) {
			// seed lookup, remember pre-image lookup
			Map<String, Formula> params =
				createFormalParamSubstitution(lookup, node, false);
			preLookup = lookup.createClone();

			// assume pre-condition!
			if (c.getPre() != null)
				assume(replace(c.getPre(), params, lookup));
		} else {
			// remember pre-image for \pre in assert's even if there's no method contract
			preLookup = lookup.createClone();
		}
		// TODO assume null, this, object arguments are "alloc" in the pre-state
		// could also assume that object fields of allocated objects are allocated

		if (node.isConstructor()) {
			// TODO field initializers
			if (hasExplicitConstructorInvocation(node.getBody())) {
				// assume the pre-condition before constructor calls
				// works around Java requirement that constructor call is first
//				assume(ContractRegistry.getPre(node));
			} else {
				// simulate super()
				// constructor must establish superclass invariant
				assume(findInvariant(getReceiver().getSuperclass()));
			}
		}

		return result;
	}

	/**
	 * Creates a substitution for the formal parameters of the given method
	 * declaration
	 * @param lookup the lookup to use
	 * @param node must be {@link #getMethod()}
	 * @param forPostcondition {@code true} will add the receiver even if
	 * {@code node} is a constructor
	 * @return
	 */
	private Map<String, Formula> createFormalParamSubstitution(L lookup,
			MethodDeclaration node, boolean forPostcondition) {
		if (node != getMethod())
			throw new IllegalArgumentException("This doesn't make sense");
		Map<String, Formula> params = new HashMap<String, Formula>();
		if (!Modifier.isStatic(node.getModifiers()) && (forPostcondition || !node.isConstructor()))
			params.put(Contract.THIS_VAR_NAME, lookup.getReceiver(getReceiver()));

		@SuppressWarnings("unchecked")
		List<SingleVariableDeclaration> parameters = node.parameters();
		for (SingleVariableDeclaration p : parameters)
			params.put(p.getName().getIdentifier(), lookup.getLocal(p.resolveBinding()));
		return params;
	}

	protected abstract Prover createProver();

	protected abstract L createLookup(AST ast);

	private boolean hasExplicitConstructorInvocation(Block body) {
		if (body == null || body.statements().isEmpty())
			// no or empty body
			return false;
		Statement first = (Statement) body.statements().get(0);
		return first instanceof ConstructorInvocation ||
			first instanceof SuperConstructorInvocation;
	}

	@Override
	public void endVisit(MethodDeclaration node) {
		if (! isNested) {
			// check post-condition for void methods (includes constructors)
			// in case not all paths declare a return explicitly (may be duplicate work)
			if (node.getAST().resolveWellKnownType("void").equals(node.resolveBinding().getReturnType())) {
				checkAndAssumePostCondition(node.getName());
			}

			if (node.isConstructor()) {
				// only need to prove invariant if we're still unpacked...
				for (Expression inv : findInvariant(getMethod())) {
					ProverResult result = check(encode(inv), node);
					if (result.getStatus() != ProverResult.Status.UNSAT) {
						ITypeBinding invClass = findDeclaringType(inv);
						String msg;
						if (invClass.equals(getReceiver()))
							// invariant declared in this class is failing
							msg = "Receiver class invariant could not be proved at end of constructor";
						else
							// include declaring superclass in error message
							msg = "Invariant for superclass " + invClass.getQualifiedName() +
							" could not be proved at end of constructor";
						// report on constructor name to avoid underlining entire body
						report(result, node.getName(), msg);
					}
				}
			}
			knowledge = null;
			lookup = null;
			preLookup = null;
		}
		popFlags();
		super.endVisit(node);
	}

	@Override
	public boolean visit(TypeDeclaration node) {
		boolean result = super.visit(node);
		pushFlags(node.resolveBinding());
		return result;
	}

	@Override
	public void endVisit(TypeDeclaration node) {
		popFlags();
		super.endVisit(node);
	}

	private void pushFlags(IBinding binding) {
		Boolean nullChecksFlag = getChecker().getNullChecksFlag(binding);
		nullCheckStack.add(isNullChecksEnabled());
		if (nullChecksFlag != null)
			nullChecks = nullChecksFlag;

		Boolean boundsChecksFlag = getChecker().getBoundsChecksFlag(binding);
		boundsCheckStack.add(isBoundsChecksEnabled());
		if (boundsChecksFlag != null)
			boundsChecks = boundsChecksFlag;
	}

	private void popFlags() {
		nullChecks = nullCheckStack.remove(nullCheckStack.size() - 1);
		boundsChecks = boundsCheckStack.remove(boundsCheckStack.size() - 1);
	}

	/*
	 * Method contracts
	 */

	@Override
	public boolean visit(ClassInstanceCreation node) {
		boolean result = super.visit(node);
		if (node.getAnonymousClassDeclaration() != null) {
			String eclipsifiedName = IntPred.class.getName().replace('$', '.');
			for (ITypeBinding i : node.resolveTypeBinding().getInterfaces()) {
				if (eclipsifiedName.equals(i.getQualifiedName()))
					// skip predicates
					return false;
			}
		}
		return result;
	}

	@Override
	public void endVisit(ClassInstanceCreation node) {
		Contract c = getChecker().getContract(node);
		if (c != null) {
			Map<String, Formula> subst = new HashMap<String, Formula>();
			// TODO outer object
			for (int i = 0; i < node.arguments().size(); ++i) {
				subst.put(c.getParams().get(i), encode((Expression) node.arguments().get(i)));
			}

			checkContract(c, subst, node, true, node);
		}

		// new object is never null
		assume(Prefix.not(Infix.equals(lookup.getName(node), Literal.NULL)));
		super.endVisit(node);
	}

	@Override
	public void endVisit(ConstructorInvocation node) {
		Contract c = getChecker().getContract(node);
		if (c != null) {
			Map<String, Formula> subst = new HashMap<String, Formula>();
			subst.put(Contract.THIS_VAR_NAME, new Local("this", getReceiver()));
			for (int i = 0; i < node.arguments().size(); ++i) {
				subst.put(c.getParams().get(i), encode((Expression) node.arguments().get(i)));
			}

			checkContract(c, subst, null, false, node);

			// constructor must establish class invariant
			assume(findInvariant(getMethod()));
		}
		super.endVisit(node);
	}

	@Override
	public void endVisit(MethodInvocation node) {
		// assume assumptions, if applicable
		// pre-conditions already assumed in visit(MethodDeclaration)
		if (/*ContractRegistry.isPre(node) ||*/ ContractRegistry.isAssume(node))
			makeUserProvidedAssumption((Expression) node.arguments().get(0));

		// post-conditions checked in endVisit(MethodDeclaration / ReturnStatement)
//		if (ContractRegistry.isPost(node))
//			checkAndAssume((Expression) node.arguments().get(0), "Could not prove post-condition");

		// null checks if desired (implicit receiver need not be checked)
		Formula receiver = null;
		boolean isStatic = isStatic(node.resolveMethodBinding());
		if (! isStatic && node.getExpression() != null) {
			receiver = encode(node.getExpression());
			if (isNullChecksEnabled())
				checkNonNull(receiver, node.getExpression());
		}

		// process invocation
		Contract c = getChecker().getContract(node);
		if (c != null) {
			Map<String, Formula> subst = new HashMap<String, Formula>();
			if (receiver != null) {
				subst.put(Contract.THIS_VAR_NAME, receiver);
			} else if (! isStatic) {
				// implicit receiver -- never null
				subst.put(Contract.THIS_VAR_NAME,
						lookup.getReceiver(getImplicitReceiver(node.resolveMethodBinding())));
			} // else no receiver

			for (int i = 0; i < node.arguments().size(); ++i) {
				subst.put(c.getParams().get(i), encode((Expression) node.arguments().get(i)));
			}

			checkContract(c, subst, node, false, node);
		}
		super.endVisit(node);
	}

	@Override
	public void endVisit(SuperConstructorInvocation node) {
		Contract c = getChecker().getContract(node);
		if (c != null) {
			Map<String, Formula> subst = new HashMap<String, Formula>();
			subst.put(Contract.THIS_VAR_NAME, lookup.getReceiver(getReceiver()));
			// TODO outer object
			for (int i = 0; i < node.arguments().size(); ++i) {
				subst.put(c.getParams().get(i), encode((Expression) node.arguments().get(i)));
			}

			checkContract(c, subst, null, false, node);

			// constructor must establish superclass invariant
			assume(findInvariant(node.resolveConstructorBinding().getDeclaringClass()));
		}
		super.endVisit(node);
	}

	@Override
	public void endVisit(SuperMethodInvocation node) {
		// process invocation
		Contract c = getChecker().getContract(node);
		if (c != null) {
			Map<String, Formula> subst = new HashMap<String, Formula>();
			if (! isStatic(node.resolveMethodBinding())) {
				subst.put(Contract.THIS_VAR_NAME, lookup.getReceiver(getReceiver()));
			} // else no receiver
			for (int i = 0; i < node.arguments().size(); ++i) {
				subst.put(c.getParams().get(i), encode((Expression) node.arguments().get(i)));
			}

			checkContract(c, subst, node, false, node);
		}
		super.endVisit(node);
	}

	/**
	 * Helper method to check contracts at invocation sites
	 * @param c contract to check
	 * @param subst Concrete arguments encoded as formulae
	 * @param result Result expression or {@code null} if checking
	 * a {@link ConstructorInvocation} or {@link SuperConstructorInvocation}
	 * @param resultIsThis {@code true} if {@code result} is also the receiver,
	 * which is the case for {@link ClassInstanceCreation}s
	 * @param node The AST node to report problems on if needed
	 * @return <code>true</code> if pre-condition was proved,
	 * <code>false</code> otherwise
	 */
	private void checkContract(Contract c, Map<String, Formula> subst,
			Expression result, boolean resultIsThis, ASTNode node) {
		// 1. assert pre-condition
		if (c.getPre() != null)
			checkAndAssume(replace(c.getPre(), subst, lookup),
					node, "Could not prove pre-condition");
		// TODO efficiency: only clone lookup if post-condition accesses pre-image
		L preImage = c.getPost() == null ? null : lookup.createClone();

		// 2. havoc anything possibly modified by method
		Map<Name, Set<IVariableBinding>> modifiable =
			new HashMap<Name, Set<IVariableBinding>>();
		// modifiable map used to havoc fields reachable by parameters with
		// modifiable permission, except parameters' fields themselves, which
		// are only modified if listed in modified sets
		// pass in those sets also (that's why modifiable is map) so we can
		// in the future do step 2b below in havocUnprotected as well
		for (Entry<String, Set<IVariableBinding>> mod : c.getModified().entrySet()) {
			Set<IVariableBinding> fields = mod.getValue();
			if (fields == null)
				// means parameter takes no modifying permission
				continue;
			// since we're modifying fields this must be an object
			Name accessor = (Name) subst.get(mod.getKey());
			modifiable.put(accessor, fields);
		}
		// TODO efficiency: do all of below in one step to reduce havocs
		// 2a. havoc unprotected heap portions
		//     rationale: if we don't have permission, maybe the callee does
		//     also unprotected if we give the callee modifiable permission
		havocUnprotected(node, modifiable);
		// 2b. havoc modified fields
		assume(lookup.havoc(modifiable));

		// 3. assume post-condition
		if (result != null)
			subst.put(resultIsThis ? Contract.THIS_VAR_NAME : Contract.RESULT_VAR_NAME,
					lookup.getName(result));
		if (c.getPost() != null)
			assume(replace(c.getPost(), subst, lookup, preImage));
	}

	@Override
	public void endVisit(Assignment node) {
		// TODO havoc rhs if excl permission assigned
		Assignment.Operator op = node.getOperator();
		Formula rhs = encode(node.getRightHandSide());
		if (!Assignment.Operator.ASSIGN.equals(op)) {
			// += etc
			// turn x += y into x = x + y
			Formula preLhs = encode(node.getLeftHandSide());
			Operator infixOp;
			if (Assignment.Operator.BIT_AND_ASSIGN.equals(op))
				infixOp = Operator.AND;
			else if (Assignment.Operator.BIT_OR_ASSIGN.equals(op))
				infixOp = Operator.OR;
			else if (Assignment.Operator.BIT_XOR_ASSIGN.equals(op))
				infixOp = Operator.XOR;
			else if (Assignment.Operator.DIVIDE_ASSIGN.equals(op))
				infixOp = Operator.DIVIDE;
			else if (Assignment.Operator.LEFT_SHIFT_ASSIGN.equals(op))
				infixOp = Operator.LEFT_SHIFT;
			else if (Assignment.Operator.MINUS_ASSIGN.equals(op))
				infixOp = Operator.MINUS;
			else if (Assignment.Operator.PLUS_ASSIGN.equals(op))
				infixOp = Operator.PLUS;
			else if (Assignment.Operator.REMAINDER_ASSIGN.equals(op))
				infixOp = Operator.REMAINDER;
			else if (Assignment.Operator.RIGHT_SHIFT_SIGNED_ASSIGN.equals(op))
				infixOp = Operator.RIGHT_SHIFT_SIGNED;
			else if (Assignment.Operator.RIGHT_SHIFT_UNSIGNED_ASSIGN.equals(op))
				infixOp = Operator.RIGHT_SHIFT_UNSIGNED;
			else if (Assignment.Operator.TIMES_ASSIGN.equals(op))
				infixOp = Operator.TIMES;
			else
				throw new IllegalArgumentException(op.toString());
			rhs = new Infix(preLhs, infixOp, rhs);
		}
		Formula lhs = equate(node.getLeftHandSide(), true /* fresh lhs */, rhs);
		// TODO effect!  havoc anything not reachable through permissions
		super.endVisit(node);

		// near-clone in endVisit(VariableDeclarationFragment) !!!!
		// if this is a EXCL lhs then inject disjointness with all names with permissions
		RefType leftType = getCurrentScope().getEffectiveType(node.getLeftHandSide());
		if (leftType != null && leftType.getPerm() == PermKind.EXCL) {
			Set<IVariableBinding> havePerms = new LinkedHashSet<IVariableBinding>();
			boolean inInstanceMethod = ! isStatic(getSignature());
			for (Entry<IVariableBinding, PermKind> other : getCurrentScope().getLocalsAndReceiverFields(false).entrySet()) {
				if (other.getValue() == null)
					// shouldn't happen
					throw new NullPointerException("Null permission for " + other.getKey());
				else if (! other.getKey().isField() || inInstanceMethod)
					// apparently fields are included even in static methods--skip 'em
					havePerms.add(other.getKey());
			}
			List<Formula> disjoint = new ArrayList<Formula>(Math.min(havePerms.size(), 16));
			Local receiver = null; // lazy resolution when needed
			for (IVariableBinding excl : havePerms) {
				Name d;
				if (excl.isField()) {
					if (receiver == null)
						receiver = lookup.getReceiver(getReceiver());
					d = lookup.getField(receiver, excl);
				} else {
					d = lookup.getLocal(excl);
				}
				if (lhs.equals(d))
					continue;
				disjoint.add(Prefix.not(Infix.equals(lhs, d)));
			}
			if (! disjoint.isEmpty())
				assume(Infix.toInfix(Operator.OR,
						Infix.equals(lhs, Literal.NULL),
						Infix.toInfix(Operator.AND, disjoint)));
		}
	}

	@Override
	public void endVisit(PostfixExpression node) {
		Name lvalue = lookup.getName(node.getOperand());
		Operator op;
		if (PostfixExpression.Operator.INCREMENT.equals(node.getOperator())) {
			op = Operator.PLUS;
		} else if (PostfixExpression.Operator.DECREMENT.equals(node.getOperator())) {
			op = Operator.MINUS;
		} else {
			throw new IllegalStateException("Non-assigning: " + node.getOperator());
		}
		Local temp = lookup.getLocal(node);
		equate(node.getOperand(), false, temp); // preserve old value in temp
		equate(node.getOperand(), true,
				new Infix(lvalue, op, Literal.getLiteral(1)));
	}

	@Override
	public void endVisit(PrefixExpression node) {
		if (AssignedFinder.ASSIGNING_PREPOST_OPS.contains(node.getOperator())) {
			Name lvalue = lookup.getName(node.getOperand());
			Operator op;
			if (PrefixExpression.Operator.INCREMENT.equals(node.getOperator())) {
				op = Operator.PLUS;
			} else if (PrefixExpression.Operator.DECREMENT.equals(node.getOperator())) {
				op = Operator.MINUS;
			} else {
				throw new IllegalStateException("Non-assigning: " + node.getOperator());
			}
			equate(node.getOperand(), true,
					new Infix(lvalue, op, Literal.getLiteral(1)));
			Local temp = lookup.getLocal(node);
			equate(node.getOperand(), false, temp); // preserve new value in temp
		} // else rely on expression encoder
		super.endVisit(node);
	}

	@Override
	public void endVisit(SingleVariableDeclaration node) {
		handleVarInitializer(node);
		super.endVisit(node);
	}

	@Override
	public void endVisit(VariableDeclarationFragment node) {
		handleVarInitializer(node);
		super.endVisit(node);
		if (node.getInitializer() == null)
			return;

		// near-clone in endVisit(Assignment) !!!!
		// if this is a EXCL lhs then inject disjointness with all names with permissions
		RefType leftType = getCurrentScope().getEffectiveType(node.getName());
		if (leftType != null && leftType.getPerm() == PermKind.EXCL) {
			Set<IVariableBinding> havePerms = new LinkedHashSet<IVariableBinding>();
			boolean inInstanceMethod = ! isStatic(getSignature());
			for (Entry<IVariableBinding, PermKind> other : getCurrentScope().getLocalsAndReceiverFields(false).entrySet()) {
				if (other.getValue() == null)
					// shouldn't happen
					throw new NullPointerException("Null permission for " + other.getKey());
				else if (! other.getKey().isField() || inInstanceMethod)
					// apparently fields are included even in static methods--skip 'em
					havePerms.add(other.getKey());
			}

			List<Formula> disjoint = new ArrayList<Formula>(Math.min(havePerms.size(), 16));
			Local lhs = lookup.getLocal(node.resolveBinding());
			Local receiver = null; // lazy resolution when needed
			for (IVariableBinding excl : havePerms) {
				Name d;
				if (excl.isField()) {
					if (receiver == null)
						receiver = lookup.getReceiver(getReceiver());
					d = lookup.getField(receiver, excl);
				} else {
					if (node.resolveBinding().equals(excl))
						// don't in-equate new variable with itself
						continue;
					d = lookup.getLocal(excl);
				}
				disjoint.add(Prefix.not(Infix.equals(lhs, d)));
			}
			if (! disjoint.isEmpty())
				assume(Infix.toInfix(Operator.OR,
						Infix.equals(lhs, Literal.NULL),
						Infix.toInfix(Operator.AND, disjoint)));
		}
	}

	private void handleVarInitializer(VariableDeclaration node) {
		if (node.getInitializer() != null)
			equate(node.getName(), false, encode(node.getInitializer()));
	}

	private Formula equate(Expression target, boolean havoc, Formula rhs) {
		Collection<Field> toEquate = getFieldsIfName(rhs);

		Formula lhs;
		if (useArrayStore && target instanceof ArrayAccess) {
			ArrayAccess select = (ArrayAccess) target;
			Formula array = encode(select.getArray());
			toEquate = getFieldsIfName(array);
			Store s = new Store(array, encode(select.getIndex()), rhs,
					select.resolveTypeBinding());
			// recursively equate surrounding array
			lhs = equate(select.getArray(), havoc, s);
		} else {
			if (havoc)
				assume(lookup.havoc(Collections.singleton(target), false));
			lhs = encode(target);
			assume(Infix.equals(lhs, rhs));
		}

		if (!toEquate.isEmpty() && lhs instanceof Name) {
			// equate fields
			if (! useArrayStore)
				throw new IllegalStateException("shouldn't get here");
			for (Field f : toEquate) {
				// this could be a lot....
				assume(Infix.equals(
						lookup.getField((Name) lhs, f.getBinding()), f));
			}
		}
		return lhs;
	}

	protected abstract Collection<Field> getFieldsIfName(Formula rhs);

	@Override
	public void endVisit(AssertStatement node) {
		if (node.getClass() != AssertStatement.class)
			// JML assume statement TODO get Spec* types "optionally" imported
			makeUserProvidedAssumption(node.getExpression());
		else
			checkAndAssume(node.getExpression(), "Could not prove assertion");
		super.endVisit(node);
	}

	@Override
	public void endVisit(ReturnStatement node) {
		checkAndAssumePostCondition(node);
		super.endVisit(node);
	}

	/**
	 * Makes the given assumption, optionally trying to prove it first
	 * if so configured with {@link JavaSypPreferences#isProveAssumptions()}
	 * @param assumption assumption to make
	 */
	private void makeUserProvidedAssumption(Expression assumption) {
		if (assumption == null)
			return;
		Formula encoded = encode(assumption);
		// if requested, try to assert the assumption, which will also assume it
		if (! JavaSypPreferences.getInstance().isProveAssumptions()
			|| ! checkAndAssume(encoded, assumption,
					"Making assumption even though it could not be proved"))
			// if we are not to prove assumptions, just assume them
			// or, if assertion fails, assume it anyway
			assume(encoded);
	}

	private void assume(Iterable<Expression> assumptions) {
		for (Expression e : assumptions)
			assume(e);
	}

	/**
	 * Encodes the given expression as an assumption formula
	 * @param assumption
	 * @see #assume(Formula)
	 */
	private void assume(Expression assumption) {
		if (assumption == null)
			return;
		Formula encoded = encode(assumption);
		assume(encoded);
	}

	protected void assume(Collection<Formula> encoded) {
		if (encoded == null || encoded.isEmpty())
			return;
		for (Formula f : encoded)
			assume(f);
	}

	/**
	 * Adds the given formula as an assumption
	 * @param encoded
	 */
	private void assume(Formula encoded) {
		if (encoded == null)
			return;
		knowledge.add(encoded);
	}

	/**
	 * Checks and assumes the {@link #getMethod() current method}'s post-condition.
	 * Predicates separated by {@code &&} are checked and assumed separately in
	 * order to provide more specific error messages.
	 * @param node {@link ReturnStatement} being checked or a node to report
	 * errors on if we are checking a default return
	 * @see #endVisit(ReturnStatement)
	 * @see #endVisit(MethodDeclaration)
	 */
	private void checkAndAssumePostCondition(final ASTNode node) {
		Contract c = getChecker().getContract(getMethod());
		if (c != null && c.getPost() != null) {
			final Map<String, Formula> params =
				createFormalParamSubstitution(lookup, getMethod(), true);

			final String msg;
			if (node instanceof ReturnStatement) {
				msg = "Could not prove post-condition: %s";
				Expression returnValue = ((ReturnStatement) node).getExpression();
				if (returnValue != null)
					params.put(Contract.RESULT_VAR_NAME, encode(returnValue));

			} else {
				msg = "Could not prove post-condition at default return: %s";
			}

			// prove top-level <p1> && <p2> && ... one at a time in order
			// this is so user can tell which post-condition failed
			// because ensures <p1>; ensures <p2>; appears as <p1> && <p2> here
			c.getPost().dispatch(new FormulaVisitor<Boolean>() {

				@Override
				public Boolean defaultVisit(Formula f) {
					// substitute parameters and \old
					Formula concrete = replace(f, params, lookup, preLookup);
					// substitute per subformula so we can use original f in error message
					return checkAndAssume(concrete, node, msg, f);
					// assume what we prove so && works as expected
				}

				@Override
				public Boolean visit(Infix f) {
					if (Operator.CONDITIONAL_AND.equals(f.getOp())) {
						// use && so we don't try to prove rhs without knowing lhs
						return f.getLhs().dispatch(this)
							&& f.getRhs().dispatch(this);
					} else {
						return defaultVisit(f);
					}
				}
			});
		}
	}

	/**
	 * Attempts to prove the given assertions and prints
	 * @param assertions
	 * @param message Error message in problem marker in case assertion fails
	 * @see #check(Formula)
	 */
	private void checkAndAssume(Collection<Expression> assertions, String message) {
		if (assertions == null || assertions.isEmpty())
			return;
		for (Expression e : assertions)
			checkAndAssume(e, message);
	}

	/**
	 * Attempts to prove the given assertion and prints
	 * @param assertion
	 * @param message Error message in problem marker in case assertion fails
	 * @see #check(Formula)
	 */
	private void checkAndAssume(Expression assertion, String message) {
		if (assertion == null)
			return;
		checkAndAssume(encode(assertion), assertion, message);
	}

	/**
	 * Attempts to prove the given assertion and prints;
	 * the predicate is assumed if it could be proved
	 * @param assertion
	 * @param node Node to report problems on
	 * @param message Error message in problem marker in case assertion fails
	 * @param args Parameters for {@link String#format(String, Object...)}
	 * @return {@code true} if assertion could be proved, {@code false} otherwise.
	 * @see #check(Formula, ASTNode)
	 */
	private boolean checkAndAssume(Formula assertion, ASTNode node, String message, Object... args) {
		ProverResult result = check(assertion, node);
		if (result.getStatus() == Status.UNSAT)
			// now that we proved it we can assume it :)
			assume(assertion);
		return report(result, node, message, args);
	}

	private boolean report(ProverResult result, ASTNode node, String message, Object... args) {
		Status status = result.getStatus();
		if (status == Status.UNSAT)
			return true;

		StringBuilder msg = new StringBuilder(status.toString()).append(": ");
		msg.append(args == null || args.length == 0 ? message : String.format(message, args));
		if (status == Status.TIMEOUT || status == Status.OTHER) {
			// include query text to give the user something to work with
			String q = result.getQuery();
			if (q != null)
				msg.append('\n').append(q);
		}
		if (JavaSypPreferences.getInstance().isCounterexamplesRequested()) {
			Collection<? extends String> ce = result.getCounterExample();
			if (ce != null && !ce.isEmpty()) {
				// include counterexample in problem marker
				for (String s : ce)
					msg.append('\n').append(s);
			}
		}
		getChecker().reportUserProblem(msg.toString(), node, Category.PROVER);
		return false;
	}

	/**
	 * Attempts to prove the given formula and returns how it went.
	 * @param assertion
	 * @return <code>true</code> if the given assertion could be proven,
	 * <code>false</code> otherwise (including if truth is unknown)
	 */
	private ProverResult check(Formula assertion, ASTNode node) {
		if (assertion == null || getChecker().isCanceled())
			return ProverResult.UNSAT;
		try {
			if (smoke && prover.check(knowledge, Literal.FALSE).getStatus() == ProverResult.Status.UNSAT)
				throw new IllegalStateException("Leads to contradiction: " + knowledge);

			ProverResult result = prover.check(knowledge, assertion);
			if (result.getWarnings() != null)
				// notify any messages or exceptions from the prover
				getChecker().reportUserProblem(result.getWarnings(), node, Category.WARN);

			return result;
		} catch (InterruptedException e) {
			// checker was interrupted, cancel the rest
			getChecker().cancel();
			Thread.currentThread().interrupt();
			return ProverResult.TIMEOUT;
		}
	}

	/** Encode given expression with current {@link #lookup} */
	private Formula encode(Expression e) {
		return getChecker().encode(e, lookup, preLookup);
	}

	/**
	 * Reports an error on the given node if the given reference may be null
	 * @param ref
	 * @param node
	 * @return {@code true} if check succeeded (ref != null), {@code false} otherwise
	 */
	private boolean checkNonNull(Formula ref, ASTNode node) {
		return checkAndAssume(Prefix.not(Infix.equals(ref, Literal.NULL)),
				node, "may be null");
	}

	/*
	 * Conditionals
	 */

	@Override
	public boolean visit(ConditionalExpression node) {
		node.getExpression().accept(this);
		Set<Formula> commonKnowledge = new LinkedHashSet<Formula>(knowledge);
		L elseLookup = lookup.createClone();
		Formula cond = encode(node.getExpression());
		Formula notCond = Prefix.not(cond);

		assume(cond); // assume condition in then branch
		node.getThenExpression().accept(this);
		equate(node, false, encode(node.getThenExpression()));
		Set<Formula> thenKnowledge = knowledge;
		L thenLookup = lookup;
		thenKnowledge.removeAll(commonKnowledge);
		// cond not needed in resulting implication so let's keep formula smaller
		thenKnowledge.remove(cond);

		knowledge = new LinkedHashSet<Formula>(commonKnowledge);
		lookup = elseLookup;
		assume(notCond); // assume ! cond in else branch
		node.getElseExpression().accept(this);
		equate(node, false, encode(node.getElseExpression()));
		Set<Formula> elseKnowledge = knowledge;
		elseKnowledge.removeAll(commonKnowledge);
		// cond not needed in resulting implication so let's keep formula smaller
		elseKnowledge.remove(notCond);

		// adjust variable names for re-assignments
		AbstractHavocLookup.mergeLookups(thenLookup, thenKnowledge, /*else*/lookup, elseKnowledge);

		// commonK & (cond ==> thenK) & (!cond ==> elseK)
		knowledge = commonKnowledge;
		if (! thenKnowledge.isEmpty())
			assume(new Infix(notCond,
					Operator.OR, Infix.toInfix(Operator.AND, thenKnowledge)));
		if (! elseKnowledge.isEmpty())
			assume(new Infix(cond,
					Operator.OR, Infix.toInfix(Operator.AND, elseKnowledge)));

		return false;
	}

	@Override
	@SuppressWarnings("unchecked")
	public boolean visit(InfixExpression node) {
		boolean superResult = super.visit(node);
		Operator op = node.getOperator();
		if (!Operator.CONDITIONAL_AND.equals(op) && !Operator.CONDITIONAL_OR.equals(op))
			return superResult;

		node.getLeftOperand().accept(this);
		Set<Formula> commonKnowledge = new LinkedHashSet<Formula>(knowledge);
		L commonLookup = lookup.createClone();

		// assume cond for && (or ! cond for ||) when checking right-hand side
		Formula cond = encode(node.getLeftOperand());
		if (Operator.CONDITIONAL_OR.equals(op))
			cond = Prefix.not(cond);
		assume(cond);
		node.getRightOperand().accept(this);

		List<Formula> conditions;
		if (node.hasExtendedOperands()) {
			conditions = new ArrayList<Formula>(node.extendedOperands().size() + 1);
			conditions.add(cond);

			Expression toAssume = node.getRightOperand();
			for (Expression e : (List<Expression>) node.extendedOperands()) {
				cond = encode(toAssume);
				if (Operator.CONDITIONAL_OR.equals(op))
					 cond = Prefix.not(cond);
				assume(cond);
				conditions.add(cond);
				e.accept(this);
				toAssume = e;
			}
		} else {
			conditions = Collections.singletonList(cond);
		}

//		equate(node, false, encode(node.getRightOperand()));
		Set<Formula> thenKnowledge = knowledge;
//		L thenLookup = lookup;
		thenKnowledge.removeAll(commonKnowledge);
		thenKnowledge.removeAll(conditions);

		// adjust variable names for re-assignments
		AbstractHavocLookup.mergeLookups(commonLookup, commonKnowledge, /*then*/lookup, thenKnowledge);
		knowledge = commonKnowledge;
		// commonK & (cond ==> thenKnowledge)
		if (! thenKnowledge.isEmpty())
			assume(new Infix(Prefix.not(Infix.toInfix(Operator.AND, conditions)),
					Operator.OR, Infix.toInfix(Operator.AND, thenKnowledge)));

		return false;
	}

	@Override
	// this implementation includes the overridden super.visit(IfStatement) code
	public boolean visit(IfStatement node) {
		node.getExpression().accept(this);
		Formula cond = encode(node.getExpression());
		Formula notCond = Prefix.not(cond);

		// save current scope, knowledge, and lookup
		boolean hasElse = node.getElseStatement() != null;
		Scope saveScope = hasElse ? new Scope(getCurrentScope()) : null;
		Set<Formula> commonKnowledge = new LinkedHashSet<Formula>(knowledge);
		L elseLookup = lookup.createClone();

		// continue using current scope, knowledge, and lookup for then
		prepareScopeVisit(node.getThenStatement());
		assume(cond); // assume condition in then branch
		node.getThenStatement().accept(this);

		// save scope, knowledge, and lookup after then
		Scope thenScope = popScope();
		Set<Formula> thenKnowledge = knowledge;
		L thenLookup = lookup;
		thenKnowledge.removeAll(commonKnowledge);
		// cond not needed in resulting implication so let's keep formula smaller
		thenKnowledge.remove(cond);

		// start fresh for else-branch
		Set<Formula> elseKnowledge;
		lookup = elseLookup;
		if (hasElse) {
			knowledge = new LinkedHashSet<Formula>(commonKnowledge);

			setCurrentScope(saveScope);
			prepareScopeVisit(node.getElseStatement());
			assume(notCond); // assume ! cond in else branch
			node.getElseStatement().accept(this);
			Scope elseScope = popScope();

			elseKnowledge = knowledge;
			elseKnowledge.removeAll(commonKnowledge);
			// notCond not needed in resulting implication so let's keep formula smaller
			elseKnowledge.remove(notCond);

			try {
				elseScope.mergeIn(thenScope);
			} catch (PermissionException e) {
				getChecker().reportUserProblem(e.getLocalizedMessage(),
						node, Category.LOCALS);
			}
			// continue using lookup and scope
		} else {
			// shortcut if there's no else branch
			elseKnowledge = new LinkedHashSet<Formula>();

			try {
				thenScope.releaseScopeVariables();
			} catch (PermissionException e) {
				getChecker().reportUserProblem(e.getLocalizedMessage(),
						node, Category.LOCALS);
			}
		}

		// adjust variable names for re-assignments
		AbstractHavocLookup.mergeLookups(thenLookup, thenKnowledge, /*else*/lookup, elseKnowledge);

		// commonK & (cond ==> thenK) & (!cond ==> elseK)
		knowledge = commonKnowledge;
		if (! thenKnowledge.isEmpty())
			assume(new Infix(notCond,
					Operator.OR, Infix.toInfix(Operator.AND, thenKnowledge)));
		if (! elseKnowledge.isEmpty())
			assume(new Infix(cond,
					Operator.OR, Infix.toInfix(Operator.AND, elseKnowledge)));

		return false;
	}

	////////////////////////////////
	//
	//  Loops
	//
	////////////////////////////////

	@Override
	public boolean visit(EnhancedForStatement node) {
		super.visit(node);

		Collection<Expression> inv = findLoopInvariant(node.getBody());

		node.getExpression().accept(this);
		if (isNullChecksEnabled())
			// iterable must not be null
			checkNonNull(encode(node.getExpression()), node);

		checkAndAssume(inv, "Could not prove loop invariant before loop entry");

		havocAssignedVariables(node);
		havocModifiableFields();
		assume(inv);
		Set<Formula> initialKnowledge = new LinkedHashSet<Formula>(knowledge);
		L initialLookup = lookup.createClone();

		// 1. check body
		node.getBody().accept(this);
		// TODO break / continue
		checkAndAssume(inv, "Could not prove loop invariant after loop body");

		// 2. keep going
		lookup = initialLookup;
		knowledge = initialKnowledge;

		return false;
	}

	@Override
	@SuppressWarnings("unchecked")
	public boolean visit(ForStatement node) {
		super.visit(node);

		Collection<Expression> inv = findLoopInvariant(node.getBody());
		for (Expression init : (List<Expression>) node.initializers()) {
			init.accept(this);
		}
		if (node.getExpression() != null) // condition can be empty!
			node.getExpression().accept(this);
		checkAndAssume(inv, "Could not prove loop invariant before loop entry (after initializers)");

		// havoc only locals assigned in the repeating part of the for statement
		Expression[] headers = new Expression[node.updaters().size() + 1];
		((List<Expression>) node.updaters()).toArray(headers);
		headers[headers.length - 1] = node.getExpression();
		havocAssignedVariables(node.getBody(), headers);
		havocModifiableFields();

		Formula cond = node.getExpression() != null ?
				encode(node.getExpression()) : Literal.TRUE;
		assume(inv);
		Set<Formula> initialKnowledge = new LinkedHashSet<Formula>(knowledge);
		L initialLookup = lookup.createClone();

		// 1. check body assuming condition
		assume(cond);
		node.getBody().accept(this);
		for (Expression update : (List<Expression>) node.updaters()) {
			update.accept(this);
		}
		checkAndAssume(inv, "Could not prove loop invariant after loop body and updaters");

		// 2. keep going assuming ! condition
		lookup = initialLookup;
		knowledge = initialKnowledge;
		// TODO can only assume this if there's no break statements....
		assume(Prefix.not(cond));

//		endVisit(node); false skips children but still causes endVisit to be called....
		return false;
	}

	@Override
	public boolean visit(DoStatement node) {
		// TODO Auto-generated method stub
		return super.visit(node);
	}

	@Override
	public boolean visit(WhileStatement node) {
		super.visit(node);

		Collection<Expression> inv = findLoopInvariant(node.getBody());
		node.getExpression().accept(this);
		checkAndAssume(inv, "Could not prove loop invariant before loop entry");

		havocAssignedVariables(node);
		havocModifiableFields();
		Formula cond = encode(node.getExpression());
		assume(inv);
		Set<Formula> initialKnowledge = new LinkedHashSet<Formula>(knowledge);
		L initialLookup = lookup.createClone();

		// 1. check body
		assume(cond);
		node.getBody().accept(this);
		// TODO break / continue
		checkAndAssume(inv, "Could not prove loop invariant after condition and loop body");

		// 2. keep going
		lookup = initialLookup;
		knowledge = initialKnowledge;
		// TODO can only assume this if there's no break statements....
		assume(Prefix.not(cond));

//		endVisit(node); false skips children but still causes endVisit to be called....
		return false;
	}

	@Override
	public boolean visit(BreakStatement node) {
		// TODO break / continue
		getChecker().reportUserProblem("loop invariants not checked", node, Category.UNSUPPORTED);
		return super.visit(node);
	}

	@Override
	public boolean visit(ContinueStatement node) {
		// TODO break / continue
		getChecker().reportUserProblem("loop invariants not checked", node, Category.UNSUPPORTED);
		return super.visit(node);
	}

	private void havocModifiableFields() {
		Contract c = getChecker().getContract(getMethod());
		Map<Name, Set<IVariableBinding>> modifiable =
			new HashMap<Name, Set<IVariableBinding>>();
		for (Map.Entry<String, Set<IVariableBinding>> mod : c.getModified().entrySet()) {
			Set<IVariableBinding> fields = mod.getValue();
			if (fields == null || fields.isEmpty())
				continue;
			String param = mod.getKey();

			Local accessor;
			if (Contract.THIS_VAR_NAME.equals(param)) {
				accessor = lookup.getReceiver(getReceiver());
			} else {
				throw new UnsupportedOperationException("loop in method with modifiable formal parameters");
			}
			if (modifiable.put(accessor, fields) != null)
				throw new IllegalStateException("Weird");
		}
		assume(lookup.havoc(modifiable));
	}

	/**
	 * @param stmt
	 * @param exprs for for loops, so we can exclude initializers;
	 * may be empty and elements may be <code>null</code>
	 */
	private void havocAssignedVariables(Statement stmt, Expression... exprs) {
		Set<Expression> assigned =
			AssignedFinder.findAssigned(stmt);
		for (Expression e : exprs) {
			if (e != null)
				assigned.addAll(AssignedFinder.findAssigned(e));
		}
		assume(lookup.havoc(assigned, true));
	}

	private Collection<Expression> findLoopInvariant(Statement body) {
		return getChecker().getLoopInvariant(body);
	}

	//////////////////////////////////
	//
	// Field access
	//
	// - default null checks (FieldAccess, QualifiedName)
	//   not needed for SimpleName b/c receiver always non-null
	// - class invariants (LabeledStatement)
	//
	//////////////////////////////////

	@Override
	public void endVisit(FieldAccess node) {
		if (isNullChecksEnabled() && node.getExpression() != null) {
			Expression obj = node.getExpression();
			Formula ref = encode(obj);
			// could special-case for this here
			checkNonNull(ref, obj);
		}
		super.endVisit(node);
	}

	@Override
	public void endVisit(QualifiedName node) {
		if (isNullChecksEnabled() && node.getQualifier() != null) {
			try {
				IVariableBinding f = (IVariableBinding) node.resolveBinding();
				if (! isStatic(f)) {
					Expression obj = node.getQualifier();
					Formula ref = encode(obj);
					checkNonNull(ref, obj);
				}
			} catch (ClassCastException e) {
				// not a field
			}
		}
		super.endVisit(node);
	}

	@Override
	public boolean visit(LabeledStatement node) {
		boolean result = super.visit(node);
		PermKind p = PermKind.valueOrNull(node.getLabel().getIdentifier().toUpperCase());
		if (p != null) {
			assume(findInvariant(getMethod()));
		}
		return result;
	}

	@Override
	public void endVisit(LabeledStatement node) {
		PermKind p = PermKind.valueOrNull(node.getLabel().getIdentifier().toUpperCase());
		if (PermKind.EXCL == p) {
			// only need to prove invariant if we may have modified something
			for (Expression inv : findInvariant(getMethod())) {
				ProverResult result = check(encode(inv), node);
				if (result.getStatus() != ProverResult.Status.UNSAT) {
					// print inv into error message
					ITypeBinding invClass = findDeclaringType(inv);
					String msg;
					if (invClass.equals(getReceiver()))
						// invariant for this class is failing
						msg = "Receiver class invariant could not be proved at end of exposure: " + inv;
					else
						// include declaring superclass in error message
						msg = "Invariant for superclass " + invClass.getQualifiedName() +
						" could not be proved at end of exposure: " + inv;
					// report on label to avoid underlining entire block
					report(result, node.getLabel(), msg);
				}
			}
		}
		super.endVisit(node);
	}

	private Collection<Expression> findInvariant(MethodDeclaration method) {
		try {
			TypeDeclaration clazz = (TypeDeclaration) method.getParent();
			// TODO should use "standalone" encoding for invariants
			return findInvariant(clazz);
		} catch (ClassCastException e) {
			// no invariant: method is part of annotation or enum
			// (actually we could probably support it for enums)
		}
		return Collections.emptyList();
	}

	private Collection<Expression> findInvariant(TypeDeclaration clazz) {
		return getChecker().getInvariants(clazz);
	}

	private Collection<Expression> findInvariant(ITypeBinding clazz) {
		if (clazz == null)
			return Collections.emptyList();
		return getChecker().getInvariants(clazz);
	}

	private ITypeBinding findDeclaringType(ASTNode node) {
		while (node != null && node.getNodeType() != ASTNode.TYPE_DECLARATION)
			node = node.getParent();
		if (node == null)
			return null;
		else
			return ((TypeDeclaration) node).resolveBinding();
	}

	/**
	 * @param node
	 * @param modifiable Map of modifiable variables with the fields that may
	 * be re-assigned; in addition, transitively reachable fields are unprotected
	 * @see Contract#getModified()
	 */
	protected abstract void havocUnprotected(ASTNode node,
			Map<Name, ? extends Collection<IVariableBinding>> modifiable);

	@Override
	public final void postVisit(ASTNode node) {
		if (isNullChecksEnabled() && node instanceof Expression) {
			Expression e = (Expression) node;
			if (e.resolveUnboxing()) {
				checkNonNull(encode(e), e);
			}
		}
		if (isConcurrentChecksEnabled())
			havocUnprotected(node, Collections.<Name, Set<IVariableBinding>>emptyMap());
		super.postVisit(node);
	}

	//////////////////////////////////////////////////
	//
	// Arrays
	//
	//////////////////////////////////////////////////

	@Override
	public void endVisit(ArrayAccess node) {
		Formula array = null;
		if (isNullChecksEnabled()) {
			array = encode(node.getArray());
			checkNonNull(array, node.getArray());
		}
		if (isBoundsChecksEnabled()) {
			if (array == null)
				array = encode(node.getArray());
			if (array instanceof Ref) {
				Field len = lookup.getField((Ref) array, null);
				Formula index = encode(node.getIndex());
				checkAndAssume(Infix.toInfix(Operator.LESS_EQUALS, Literal.ZERO, index),
						node.getIndex(), "may be below bounds (negative)");
				checkAndAssume(Infix.toInfix(Operator.LESS, index, len),
						node.getIndex(), "may be above bounds");
			} else {
				// TODO multi-dimensional arrays
				getChecker().reportUserProblem("Cannot check array bounds of intermediary array",
						node, Category.UNSUPPORTED);
			}
		}
		super.endVisit(node);
	}

	/**
	 * @param node
	 * @return {@code true} if given node is {@link Assignment} target,
	 * {@code false} otherwise
	 */
	@SuppressWarnings("unused")
	private static boolean isAssignmentTarget(ASTNode node) {
		if (node == null)
			return false;
		ASTNode parent = node.getParent();
		if (parent instanceof Assignment)
			return ((Assignment) parent).getLeftHandSide() == node;
		return false;
	}

	@Override
	public void endVisit(ArrayCreation node) {
		skip_default_content:
		if (node.getInitializer() == null) {
			Expression l = (Expression) node.dimensions().get(0);
			Formula length = encode(l);

			// check given length is positive
			if (isBoundsChecksEnabled()) {
				checkAndAssume(Infix.toInfix(Operator.LESS_EQUALS, Literal.ZERO, length),
						l, "may be below bounds (negative)");
				for (int i = 1; i < node.dimensions().size(); ++i) {
					Expression li = (Expression) node.dimensions().get(i);
					Formula dim = encode(li);
					checkAndAssume(Infix.toInfix(Operator.LESS_EQUALS, Literal.ZERO, dim),
							li, "may be below bounds (negative)");
				}
			}

			// inject length information
			// for simplicity only worry about outermost array dimension
			Ref array = (Ref) encode(node);
			Formula lhs = lookup.getField(array, null);
			assume(Infix.equals(lhs, length));

			// new array is never null
			assume(Prefix.not(Infix.equals(array, Literal.NULL)));

			// inject null / 0 content info
			ITypeBinding elementType = node.resolveTypeBinding().getComponentType();
			final Formula defaultValue;
			if (elementType.isPrimitive()) {
				defaultValue = Literal.getDefaultInitializer(elementType);
				if (defaultValue == null)
					break skip_default_content;
			} else if (elementType.isArray() && 1 < node.dimensions().size()) {
				// TODO initialized nested arrays, e.g., new int[5][3]
				break skip_default_content;
			} else {
				// this includes uninitialized nested arrays, e.g., new int[5][]
				defaultValue = Literal.NULL;
			}
			Local k = new Local("k-", node.getAST().resolveWellKnownType("int"));
			assume(Quantifier.forall(
				k,
				Infix.or(
					Prefix.not(Infix.and(
						Infix.toInfix(Operator.LESS_EQUALS, Literal.ZERO, k),
						Infix.toInfix(Operator.LESS, k, lhs))),
					Infix.equals(lookup.getSelect(array, k, elementType), defaultValue))));
		} else {
			equate(node, false, encode(node.getInitializer()));
		}
		super.endVisit(node);
	}

	@Override
	@SuppressWarnings("unchecked")
	public void endVisit(ArrayInitializer node) {
		List<Expression> expressions = node.expressions();
		List<Formula> formulae = new ArrayList<Formula>(expressions.size());
		for (Expression e : expressions) {
			formulae.add(encode(e));
		}

		// inject length information
		Formula length = Literal.getLiteral(node.expressions().size());
		Ref array = (Ref) encode(node);
		Formula lhs = lookup.getField(array, null);
		assume(Infix.equals(lhs, length));

		// inject content information
		for (int i = 0; i < formulae.size(); ++i) {
			assume(Infix.equals(lookup.getSelect(
					array,
					Literal.getLiteral(i),
					expressions.get(i).resolveTypeBinding()),
				formulae.get(i)));
		}

		// new array is never null
		assume(Prefix.not(Infix.equals(array, Literal.NULL)));

		super.endVisit(node);
	}

	private boolean isNullChecksEnabled() {
		return nullChecks;
	}

	private boolean isBoundsChecksEnabled() {
		return boundsChecks;
	}

	private boolean isConcurrentChecksEnabled() {
		return concurrentChecks;
	}

	/**
	 * This may be useful if variables are havoc'ed by the theorem prover.
	 * Lookup object that doesn't support havoc'ing.
	 * @author kevin
	 * @since Feb 10, 2010
	 */
	@SuppressWarnings("unused")
	private static class SimpleLookup implements ExpressionEncoder.Lookup {

		private static int nextTemp = 0;

		private final Map<Expression, Local> temps =
			new HashMap<Expression, Local>();

		@Override
		public Field getField(Ref accessor, IVariableBinding field) {
			if (accessor == null) {
				// FIXME resolution for inner classes
				accessor = new Local("this", field.getDeclaringClass());
			}
			return new Field(accessor, field);
		}

		@Override
		public Name getName(Expression e) {
			if (e instanceof ThisExpression) {
				return new Local(e.toString(), e.resolveTypeBinding());
			}
			if (e instanceof SimpleName) {
				if (! (((SimpleName) e).resolveBinding() instanceof IVariableBinding))
					throw new IllegalArgumentException("not a variable: " + e);
				IVariableBinding var = (IVariableBinding) ((SimpleName) e).resolveBinding();
				if (var.isField())
					return getField(null, var);
				else
					return new Local(e.toString(), e.resolveTypeBinding());
			}
			Local temp = temps.get(e);
			if (temp == null) {
				temp = new Local("temp" + (nextTemp++), e.resolveTypeBinding());
				temps.put(e, temp);
			}
			return temp;
		}

		@Override
		public Select getSelect(Formula array, Formula index,
				ITypeBinding elementType) {
			return new Select(array, index, elementType);
		}
	}
}
